Let us start with a simple synchronous multi–agent system. Thanks to the synchronicity, there is not a global mechanism, which prevents several automatons from performing an action at exactly the same time by executing a synchronised statement, see Synchronisation for details.

Let there be three trains which share a common track in a narrow tunnel at a certain part of their otherwise disjoint routes. We need a signalling system which prevents two or more trains from entering the common segment at the same time. The signalling is provided by a special automaton Environment. There is only a single environment in a system of agents, and the environment differs from an agent automaton in that its state can be made visible anywhere.

Let us declare, that we define an interpreted system, which is a kind of a synchronous partially observable Markov decision process:

    //
    // Test "Faulty train protocol" for any number of trains.
    //
    class pomdp sync;

An asynchronous equivalent, i.e. an interleaved interpreted system, does not take the sync keyword.

The Verics' assembly language is mostly related 1:1 to the automata generated, and thus, in order to vary the number of trains at the change of a constant value, we need a preprocessor. The preprocessor is simply an interpreter of the same Verics language used elsewhere within the Verics environment.

Let us declare the said constant:

    // number of trains
    common Z NUM := 3;

A constant like that, if precedes all preprocessor directives, is visible by both the preprocessor and the automatons.

Let the environment feature a lock (a railway signal, a semaphore), toggled to red if one of the trains arrives at the common track. If the train leaves the track, the semaphore is switched back to green.

    environment {
        Z{GREEN, RED} lights := GREEN;

    #for Z i~ := 1; i <= NUM - 1; ++i {
        [out${i}] lights == RED   -> lights := GREEN;
        [in${i}]  lights == GREEN -> lights := RED;
    #}
    };

Let's look at the same definition, yet expanded by the preprocessor:

    environment {
        Z{GREEN, RED} lights := GREEN;

        [out1] lights == RED   -> lights := GREEN;
        [in1]  lights == GREEN -> lights := RED;
        [out2] lights == RED   -> lights := GREEN;
        [in2]  lights == GREEN -> lights := RED;
    };

The identifiers in square brackets define labels, here the action ones (without sync, they would be synchronisation labels). Two automatons may synchronise, if they perform the same action. Then we have boolean equations, which guard the following updates to the state vector. A false guard unconditionaly prevents an action from happening, a true guard does not force by itself the update.

We see, that the environment can perform two actions environment.in1 and environment.in2, that allow the trains 1 and 2 to enter. Yet, we defined NUM := 3, and thus, what about the third train? It is faulty, and ignores the environment's actions completely, what translates to its ignorance about the tunnel's semaphore.

Let the definiton of all trains be as follows:

    #for Z i~ := 1; i <= NUM; ++i {
    agent train${i} { 
        Z{WAIT, TUNNEL, AWAY} phase := AWAY;

        []              true -> true;
        [approach${i}]  phase == AWAY   -> phase := WAIT;
        // the train NUM is faulty
        [${"in"  + i}]  phase == WAIT   -> phase := TUNNEL;
        [${"out" + i}]  phase == TUNNEL -> phase := AWAY;  
    };

    def in_tunnel${i} := train${i}.phase == TUNNEL;

    #}

We see, that all trains are the same including the faulty one. The difference is, that the faulty train's actions train3.in3 and train3.out3 do not have their counterparts in the environments, i.e. there are no actions environment.in3 and environment.out3. The statement beginning with def is a formula, which will allow a more terse property definition later.

Let us model–check the model. The engineer at the train 1 would want to be always assured, that no crash is possible:

    property CTL*K test_train1 := !AG(K(train1,
    #B first~ := T;
    #for Z a~ := 1; a <= NUM; ++a {
    #    for Z b~ := 1; b <= NUM; ++b {
    #        if a < b  {
                 ${first ? "" else "&&"} (!in_tunnel${a} || !in_tunnel${b})
    #            first := F;
    #        }
    #    }
    # }
    )); 

which is expanded by the preprocessor into

    property CTL*K test_train1 := !A G(K(train1,
                    (!in_tunnel1 || !in_tunnel2)
                 && (!in_tunnel1 || !in_tunnel3)
                 && (!in_tunnel2 || !in_tunnel3)
    ));

Files:

• FTC.vxs: the source of the model;
• FTC.ispl: the resulting ISPL file.

Command line:

• veric -L -oi FTC.vxs